(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Ss -> Sk *)

(* 侧滑角β (sidelip angle) *)
Parameter beta : R.

(* 迎角 α  (angle of attack) *)
Parameter alpha : R.

(* γ  *)
Parameter gamma : R.

(* Sk在飞机对称面转动 μ度 得到S' *)
Definition coordinate_transform_SaSk : Mat R 3 3 := mkMat_3_3
  1       0          0
  0  (cos gamma)  (sin gamma)
  0  (-sin gamma) (cos gamma).

Definition coordinate_transform_SsSa : Mat R 3 3 := mkMat_3_3
  (cos beta)   (sin beta)   0
  (-sin beta)  (cos beta)   0
       0           0        1.

Definition SsToSk : Mat R 3 3 := mkMat_3_3
  (cos beta)                       (sin beta)             0
  (-(cos gamma)*(sin beta)) ((cos gamma)*(cos beta)) (sin gamma)
  ((sin gamma)*(sin beta)) (-(sin gamma)*(cos beta)) (cos gamma).

Lemma SsToSk_eq:
  SsToSk === RMmul coordinate_transform_SaSk coordinate_transform_SsSa.
Proof.
  unfold SsToSk.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3. ring. f_equal. ring.
Qed.

